Zero to a non-real power is defined where its real part is positive - #1866

Fixes #1865.

Simplify turned 0 * b^i and b^i - b^i into NaN. As a result, Differentiate returned NaN for x * b^i, and for every antiderivative with a constant like (e^a)^i in it, such as sec(a + i*ln(x))^3's. Those answers were right, but they could not be differentiated back.

A power's domain condition was not b = 0 or w > 0. For a non-real number w, w > 0 has no value, because the complex numbers are not ordered. 0^w is defined where Re(w) > 0, which is what 0^w's own simplification already decides. For a numeric exponent, the condition now reads the real part. A symbolic exponent keeps w > 0.

Measured on master 8bdfcfe and on 2.5.0, which agree:

Rubi corpus, compared with master 8bdfcfe:

• Pocket of all of 4.7.5, 4.7.7 and 2.3 (1,520 problems): 1442 → 1448 solved, with 0 wrong on either side.
• The 6 that moved are x^k tan(a + i ln x) and x^k cot(a + i ln x). On master their answers were verified only after an extra Simplify; on this branch they verify directly. Each was re-run on its own.
• Every family is unchanged.

The allocation gate passed. The suite passed: 15,302 passed, 0 failed, run alone after memguard stopped the chained run at 8.2 GB.

🤖 Generated with Claude Code

https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura